A:Type, f:(A), L:A List. (1of(split_tail(L | x.f(x))) @ 2of(split_tail(L | x.f(x)))) = L 

latex

Definitions	t  T, , x:A. B(x), x. t(x), split_tail(L | x.f(x)), P  Q, x(s), as @ bs, Prop, b, A, b, P & Q, P  Q, Unit
Lemmas	eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, assert wf, append wf, split tail wf, bool wf